<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/x
html1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="content-type"
      content="text/html ; charset=US-ASCII" />
<title>Release Notes for Kananaskis-4 version of HOL 4</title>
</head>

<body>
<h1>Notes on HOL 4, Kananaskis-4 release</h1>

<h2 id="contents">Contents</h2>
<ul>
  <li> <a href="#new-features">New features</a> </li>
  <li> <a href="#bugs-fixed">Bugs fixed</a> </li>
  <li> <a href="#new-theories">New theories</a> </li>
  <li> <a href="#new-tools">New tools</a> </li>
  <li> <a href="#new-examples">New examples</a> </li>
  <li> <a href="#incompatibilities">Incompatibilities</a> </li>
</ul>



<h2 id="new-features">New features:</h2>

<ul>
  <li> There is a new unambiguous notation for set comprehensions that
  allows one to specify exactly what variables can &ldquo;vary&rdquo;
  to generate the set.  For example, the current notation interprets
<pre>
         { x + y | x &lt; y }
</pre>
      as the set that takes all pairs of numbers such that the first
      component is less than the other, and then sums them (generating
      the set of all non-zero numbers).  The new notation allows one
      to specify that only the <code>x</code> should vary by writing
<pre>
         { x + y | x | x &lt; y }
</pre>
      This denotes the set of numbers from <code>y</code> up to but not
      including <code>2&nbsp;*&nbsp;y</code>.  To express the first set
      in the new notation, one would write
<pre>
         { x + y | x,y | x &lt; y }
</pre>
      The parser accepts both notations.  The pretty-printer prefers
      the old notation unless it can not express the set being
      printed.  Further details are in the Description.  Thanks to
      John Harrison for discussion leading to the adoption of this
      syntax. </li>

  <li> <p> The syntax of string and character literals is now the same as
      that accepted by SML.  This means that escapes such as
      <code>\n</code> (for the linefeed character) and
      <code>\^E</code> (for ASCII character no.&nbsp;5) can be used
      inside string and character literals.</p>

      <p> The SML syntax which allows strings to be broken over
      new-lines by using back-slashes is also supported.  This means
      that one can write </p>
<pre>
         ``mystring = "the quick brown fox jumps over \
                      \the lazy dog"``
</pre>
      <p> and have the actual string value generated exclude the
      white-space appearing between the back-slashes.</p>
      </li>


  <li> <p> It is possible to include both <code>^</code> (caret) and
      <code>`</code> back-tick characters inside quotations.  Usually
      these characters have special meaning inside quotations: caret
      is used to introduce an antiquotation, and the back-tick is used
      to end a quotation (singly or doubly, depending on the sort of
      quotation).  The caret character can be used <em>as is</em> if a
      sequence of them is followed by white-space.  Otherwise, it
      needs to be &ldquo;escaped&rdquo; by preceding it with another
      caret character.  Similarly, the backquote character can be
      written by escaping it with a caret. For example, writing</p>
<pre>
         ``s1 ^ s2``
</pre>
      <p> will result in the string <code>s1 ^ s2</code> being passed
      to the HOL parser.  This string will then be treated in the
      standard fashion.  E.g., if <code>^</code> is an infix, a
      function application with it as the head operator will be
      created.  If one wrote <code>``s1 ^^ s2``</code> this would also
      pass through unchanged.  However, if one wrote </p>
<pre>
         ``s1 ^s2``
</pre>
      <p> this would be taken as an anti-quotation of SML variable
      <code>s2</code>.  One should write </p>
<pre>
         ``s1 ^^s2``
</pre>
      <p> to get the single caret passed to the underlying lexer.</p>

      <p> Note that the back-quote character always needs to be
      escaped by a caret, and that caret-escapes need to be applied
      even within string literals and comments that occur inside
      quotations.</p></li>


  <li> <p> The XEmacs editor is now supported, in addition to Emacs,
      by the <code>tools/hol98-mode.el</code> file of Emacs
      extensions.</p>
  </li>


  <li> <p> Case expressions may now include literals as patterns,
      in addition to constructor expressions as in the past.  These
      literals may be for example of types <code>num</code>,
      <code>char</code>, or <code>string</code>;
      or they may be of any other type as well, even function types.
      Literals need not be constants, but they must not contain
      any free variables.</p>
<pre>
         case n of
            0 -> "none"
         || 1 -> "one"
         || 2 -> "two"
         || _ -> "many"
</pre>
      <p>Patterns in case expressions are similar to the patterns used
      in the definition of recursive functions by <code>Define</code>.
      Thus they may be deeply nested within larger patterns.
      As before, in case of overlapping patterns, the earliest
      listed pattern is matched.</p>

      <p>If the set of patterns specified is sparse, there may be new
      rows generated automatically to fill it out, and possibly some new
      or renamed variables or the <code>ARB</code> constant to properly
      represent the case expression. </p>
<pre>
         - ``case a of
                (1, y, z) -> y + z
             || (x, 2, z) -> x - z
             || (x, y, 3) -> x * y``;
         > val it =
             ``case a of
                  (1,2,3) -> 2 + 3
               || (1,2,z) -> 2 + z
               || (1,y,3) -> y + 3
               || (1,y,z) -> y + z
               || (x,2,3) -> x - 3
               || (x,2,z') -> x - z'
               || (x,y',3) -> x * y'
               || (x,y',z') -> ARB`` : term
</pre>
      <p>A complex pattern with several components may include
      both literals and constructor expressions as subpatterns.
      However, a set of patterns specified in a case expression
      may not have both literals and constructor expressions as
      alternatives to each other, except insofar as a pattern
      may be both a literal and a (0-ary) constructor, such as
      the literal <code>0</code>.  See the Description for more
      information and examples of case expressions. </p>

      </li>


  <li> <p> Inductive definitions are now made with respect to a
      varying &ldquo;<code>monoset</code>&rdquo;: a list of theorems
      specifying that boolean operators are monotone in their
      arguments.  These are used to justify recursions that may occur
      underneath new operators that users introduce.  </p>

      <p> Initially, this set includes results for the standard
      boolean operators (such as existential quantification and
      conjunction), and is augmented as later theories are loaded. For
      example, the constant <code>EVERY</code> in the theory of lists,
      has a monotonicity result</p>
<pre>
         |- (!x:'a. P x ==> Q x) ==> (EVERY P l ==> EVERY Q l)
</pre>
<p> and this is incorporated into the global <code>monoset</code> when
the theory of lists is loaded.  This then allows the easy definition
of relations that recurse under <code>EVERY</code>, as in this rule
</p>
<pre>
         !x. EVERY newrel (somelist_of x) ==> newrel x
</pre>


      <p> Theorems can be declared as monotonicity results using the
      <code>export_mono</code> function.  See the Description for the
      exact form that monotonicity theorems must take. </p>

      </li>


  <li> <p>Types that are instances of abbreviation patterns (made with
      <code>type_abbrev</code>) now print in abbreviated form by
      default.  For example, if one writes</p>
<pre>
         type_abbrev("set", ``:'a -> bool``);
</pre>

      <p> Then, as before, one can write <code>``:num set``</code> and
      have this understood by the type parser.  Now, in addition, when
      types are printed, this is reversed, so that the following
      works: </p>
<pre>
         - type_of ``(UNION)``;
         > val it = ``:'a set -> 'a set -> 'a set`` : hol_type
</pre>

      <p> Unfortunately, with this particular example, one also
      gets</p>
<pre>
         - type_of ``(/\)``;
         > val it = ``:bool -> bool set`` : hol_type
</pre>

      <p> which is more confusing than it is illuminating.  For this
      reason, it is possible to turn abbreviation printing off
      globally (using a <code>trace</code> variable,
      <code>print_tyabbrevs</code>), or on an
      abbreviation-by-abbreviation basis.  The latter is done with the
      function</p>

<pre>
         disable_tyabbrev_printing : string -> unit
</pre>

      <p> Calls to this function are made in the <code>pred_set</code>
      and <code>bag</code> theories so that those theories&rsquo;
      abbreviations (<code>set</code>, <code>bag</code> and
      <code>multiset</code>) are not printed. </p>
  </li>



  <li> <p> There is a new polymorphic type,
      <code>``:'a&nbsp;itself``</code> containing just one value for
      all possible instantiations of <code>``:'a``</code>.  This value
      is supported by special syntax, and can be written</p>
<pre>
         (:tyname)
</pre>

      <p> This type provides a convenient method for defining values
      that are dependent on just the type, and not on any values
      within that type.  For example, within the <a
      href="#wordsTheory">new theory of words</a>, the constant
      <code>dimindex</code> has type
      <code>:'a&nbsp;itself&nbsp;->&nbsp;num</code>, and returns the
      cardinality of the universe of the type <code>'a</code> if the
      universe is finite, or one otherwise.  The syntax support means
      one can write terms such as </p>
<pre>
         dimindex(:bool)
</pre>
      <p> and </p>
<pre>
         dimindex(:'a -> bool)
</pre>
      <p> This type is inspired by a similar one in Isabelle/HOL.</p>
  </li>

</ul>

<h2 id="bugs-fixed">Bugs fixed:</h2>

<ul>
  <li> <p> The <code>muddyC/muddy.c</code> file would not build with
      <code>gcc-4</code>. </p>
  </li>

  <li> <p> The implementation of <code>Q.EXISTS</code> was incorrect
      (would only work with witnesses of type <code>:bool</code>).
      Thanks to Eunsuk Kang for the report of this bug. </p> </li>

  <li> <p> The natural number and integer decision procedures were not
      normalising multiplicative expressions as much as they should,
      causing obvious goals to not get proved.  Thanks to Alexey
      Gotsman for the report of this bug. </p> </li>

  <li> <p> The theory and identifier indexes in the help pages were
      generated with bogus links.  Thanks to Hasan Amjad for the
      report of this bug. </p> </li>

  <li> <p> Expressions using <code>case</code>-expressions with
      function-types and applied to arguments failed to parse
      correctly. </p> </li>

  <li> <p> The implementation of <code>Holmake</code>&rsquo;s
      <code>--rebuild_deps</code> (or <code>-r</code>) option was
      faulty.  Thanks to Tom Ridge for the report of this bug. </p>
      </li>

  <li> <p> The implementation of <code>stringLib.string_EQ_CONV</code>
      failed if one of the string arguments was the empty string.
      Thanks to Mike Gordon for the report of this bug. </p> </li>

  <li> <p> The derivation of &ldquo;strong&rdquo; induction principles
      in the inductive definitions library has been improved to cope
      with multiple (mutually recursive) inductively-defined
      relations.  Such relations could always be defined using
      <code>Hol_reln</code>, but their strong induction principles
      couldn&rsquo;t be derived.  (See below for a change in the type
      and home of this function.) </p></li>

</ul>


<h2 id="new-theories">New theories:</h2>
<ul>
  <li> <p> A theory of the rational numbers, thanks to Jens
  Brandt. This is used in the <a href="#acl2">embedding of ACL2 in
  HOL</a>.</p> </li>

  <li id="wordsTheory"> <p> A new polymorphic theory of fixed-width
  words, called <code>words</code>.  This is now our recommended way
  of using types such as <code>word32</code>, <code>word16</code> etc.
  This builds on John Harrison&rsquo;s &ldquo;Finite cartesian
  products&rdquo; from <cite>A HOL theory of Euclidean space</cite> in
  TPHOLs&nbsp;2005.  </p>

      <p> There is now no need to use the word functor
  approach introduced in Kananaskis-3 (though this code is still
  available).  Instead, when <code>wordsTheory</code> is loaded, one
  set of polymorphic constants is defined, and these can be used for
  all the word types.  Words are polymorphic in one argument (thus
  there is a type <code>``:'a&nbsp;word``</code>) and types such as
  <code>word32</code> and <code>word16</code> instantiate the type
  parameter to different concrete type arguments.  (The cardinality of
  the parameter&rsquo;s universe indicates the number of bits in the
  word.)  For more, see the Description.</p></li>

</ul>

<h2 id="new-tools">New tools:</h2>

<ul><li>None this time!</li></ul>

<h2 id="new-examples">New examples:</h2>

<ul>
  <li id="acl2"> A deep embedding
  of the entire ACL2 logic in HOL has been defined via a theory
  <code>sexp</code> of S-expressions. All 78 ACL2 axioms have been
  verified in HOL.  A suite of tools is available to translate HOL
  datatypes into S-expressions and HOL functions to functions on
  S-expressions. Scripts are provided to print S-expressions defined
  inside HOL to defuns and defthms for processing by the ACL2 system,
  and for slurping ACL2 defuns and defthms into HOL. This work is a
  collaboration between Mike Gordon and James Reynolds at the
  University of Cambridge and Warren Hunt and Matt Kaufmann at the
  University of Texas. The goal is to provide a robust and scalable
  link between the HOL4 and ACL2 systems suitable for use on
  substantial industrial-scale verification projects. </li>

<li id="temporal_deep">The example <code>temporal_deep</code> contains deep embeddings of temporal logics and other formalisms related to model checking. Amongst others there are deep embeddings of
<ul>
	<li>LTL</li>
	<li>CTL*</li>
	<li>nondeterministic and universal omega-automata</li>
	<li>alternating automata.</li>
</ul>
Additionally, there is an automated translation from LTL to omega-automata. Together with the interface to SMV from <code>temporalLib</code> this allows LTL model checking. Moreover, there is a translation of a subset of the FL of the PSL example into LTL. Thus, this example allows model checking for a subset of PSL.
</li>

</ul>

<h2 id="incompatibilities">Incompatibilities:</h2>

<ul>

  <li> <p> The <code>std_ss</code> simpset has become more powerful,
      picking up a set of &ldquo;obvious&rdquo; rewrites that used to
      be in <code>arith_ss</code>.  Now the latter simpset adds just
      the decision procedure for Presburger arithmetic.</p> </li>

  <li> <p> Functions such as <code>induction_of</code> in the
      <code>TypeBase</code> structure that used to take a string (the
      name of a type operator), now take a type.  Thus, instead of</p>
<pre>
         TypeBase.induction_of "num"
</pre> use
<pre>
         TypeBase.induction_of ``:num``
</pre>
</li>

  <li> <p> The normalisation of arithmetic terms performed by
      the <code>ARITH_ss</code> simpset fragment (and thus, the
      simpset <code>bossLib.arith_ss</code>) is more aggressive.  This
      can break proofs.  The <code>bossLib</code> library now exports
      <code>old_arith_ss</code> and <code>old_ARITH_ss</code>
      entry-points if users wish to avoid having to adjust their
      proofs. </p> </li>

  <li> <p> The <code>derive_strong_induction</code> function has
  changed type, and location.  It is now an entry-point in
  <code>IndDefLib</code>, and has type </p>
<pre>
         thm * thm -> thm
</pre>
      <p> rather than </p>
<pre>
         thm list * thm -> thm
</pre>
      <p> The first argument should now be the &ldquo;rules&rdquo;
      theorem returned by a call to <code>Hol_reln</code>. </p> </li>

<li> <p> In order to avoid certain misleading scenarios, the type of
    <code>mk_oracle_thm</code> has changed so that it takes a string
    as its first argument rather than a <code>tag</code>.  The
    implementation of <code>mk_oracle_thm</code> turns the given
    string into a tag value using the function
    <code>Tag.read</code>. There is also a new function,
    <code>Thm.add_tag</code>, that allows arbitrary tags to be added
    to existing theorems. Thanks to Mark Adams for discussion leading
    to this change. </p> </li>


</ul>




<hr />

<p> <em><a href="http://hol.sourceforge.net">HOL 4, Kananaskis-4</a></em> </p>

</body> </html>
